/*
 * Alloy Analyzer
 * Copyright (c) 2002 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

package alloy.type;

import java.util.ArrayList;
import java.util.Collection;
import java.util.Collections;
import java.util.HashSet;
import java.util.Iterator;
import java.util.LinkedHashSet;
import java.util.List;
import java.util.Set;

import alloy.ast.Expr;
import alloy.util.Dbg;

/**
 * Represents a union type, a sum of products of {@link BasicType}s.  
 * (i.e. a sum of {@link RelationTypes}).  All expressions in a 
 * semantically correct Alloy model have a UnionType associated with
 * them.
 * <p>UnionType may contain RelationTypes of different arity, or no RelationTypes at all.
 * No UnionType u can contain two RelationTypes rt1 and rt2 such that rt1 & rt2 is non-empty.
 * Furthermore, a UnionType cannot contain RelationTypes rt1, rt2, ..., rtn such that 
 * the sum rt1+rt2+...+rtn is equivalent to a single RelationType rt. 
 *
 * @see alloy.ast.HasType
 */

public class UnionType {
    
    /** set of Integers, which represent arities of RelationTypes contained in this UnionType **/
    private Set _arities = new HashSet();

    /** set of RelationType contained in this UnionType **/
    private Collection _relationTypes = new LinkedHashSet();

    /** 
     * Constructs a UnionType with no RelationTypes (size 0, arity 0)
     **/ 
    public UnionType() {}

    /**
     * Constructs the UnionType ut = {rt}
     * @param rt the first relation type of this
     */
    public UnionType(RelationType rt) {
	Dbg.check(rt != null, 
		  "attempted to create a union type with a null relation type");
	_relationTypes.add(rt);
	_arities.add(new Integer(rt.arity()));
    }

    /**
     * Constructs a UnionType that's identical to ut
     **/
    public UnionType(UnionType ut) {
	Dbg.check(ut != null, "attempted to create a union type from null");
	_relationTypes.addAll(ut._relationTypes);
	_arities.addAll(ut._arities);
    }

    /**
     * Adds rt_ to this, keeping this normalized
     * rt_ cannot be null
     */
    private void addRelationType(RelationType rt) {

	

	if (this._arities.add(new Integer(rt.arity()))) { // first RelationType of arity rt.arity()
	    this._relationTypes.add(rt);
	} else  { 
		    
	    // remove all subsets of rt in this, if any
	    // if rt is a subset of a RelationType in this, return
	    for (Iterator rIter = this.getTypeIter(); rIter.hasNext(); ) {
		RelationType relType = (RelationType) rIter.next();
		
		if (rt.isSubsetOf(relType)) return;
		if (relType.isSubsetOf(rt)) {
		    rIter.remove();
		}
	    
	    }
	    
	    // replace all ocurrences of A1->B->... + ... + An->B->... with 
	    // a single RelationType A->B-> ... whenever A is an abstract type
	    // such that A = A1 + A2 + ... + An.  Repeat this collapsing 
	    // procedure along each column, until the RelationType rtAdd that
	    // subsumes {rt} + {RelationTypes of this} is generated.  Note that
	    // RelationTypes can be folded only along ONE column at a time
	    // (i.e. one column will contain pieces of an abstract sig type
	    // while all the other columns MUST be identical -- otherwise,
	    // the sum of the RelationTypes being folded and the produced 
	    // RelationType will not represent the same sets of tuples).
	    // Also note that rtAdd cannot be either a subset or a superset
	    // of any remaining RelationTypes in this (easy to prove).
	    // For example, suppose this = {D00->C0+ D1->C0 + D->C1} where
	    // all the basic types are abstract and we have the following
	    // subtyping relations:  D00 and D01 are subtypes of D0, D0 and
	    // and D1 are subtypes of D, and C0 and C1 are subtypes of C.
	    // Now, let rt = D01->C0.  We get the sequence of foldings
	    // shown below:
	    // {D00->C0 + D1->C0 + D->C1} + D01->C0 = 
	    // {D1->C0 + D->C1} + D0->C0 =
	    // {D->C1} + D->C0 = D->C
	    RelationType rtAdd = rt;
	    for (int i = 0; i < rtAdd.arity(); i++) {
		
		while (true) {
		    BasicType bt = rtAdd.getBasicTypeAt(i);
		    if (_hasAbstractSuperType(bt)) {
			
			Collection collapsible = 
			    _getCollapsible(this._relationTypes, rtAdd, i);
			RelationType folded = _foldCollapsible(collapsible, i);
			
			if (folded != null) {
			    this._relationTypes.removeAll(collapsible);
			    rtAdd = folded;
			    continue;
			} 
		    } 
		    break;
		} 
	    }
	    this._relationTypes.add(rtAdd);
	}
    }

    /**
     * We assume that rts obeys the spec of the Collection returned by _getCollapsible. This
     * procedure will check if the set of SigTypes at position i in each rt from rts 
     * contains the set of all subtypes of their common abstract parent.  If this is
     * the case, then all the RelationTypes in the list can be replaced by a single
     * RelationType which has the abstract parent in the ith column (and the BasicTypes
     * contained in the RelationTypes of rts_ in all other columns),
     * @return a RelationType rt which is equivalent to rts[0]+rts[1]+...+rts[n], if
     * possible; otherwise returns null
     **/
    private static RelationType _foldCollapsible(Collection rts, int i) {
	if (rts.size() > 1) {

	    RelationType model = (RelationType) rts.iterator().next();
	    SigType stAbstract = ((SigType) model.getBasicTypeAt(i)).getSuperType();
	    Collection subs = new ArrayList(stAbstract.getSubTypes());
	    
	    for (Iterator iter = rts.iterator(); iter.hasNext() ; ) {
		subs.remove(((RelationType) iter.next()).getBasicTypeAt(i));
	    }
	    
	    if (subs.isEmpty()) {
		List bTypes = new ArrayList(model.getBasicTypes());
		bTypes.set(i, stAbstract);
		return new RelationType(bTypes);
	    }
	}
	return null;
    }

    /**
     * @return a Collection which contains rt and all the RelationTypes rt' from rts_ 
     * such that rt'(j) == rt(j) for j!=i and rt'(j).getSuperType() == rt.getSuperType()
     * for j==i. 
     **/
    private static Collection _getCollapsible(Collection rts, RelationType rt, int i) {
	List ret = new ArrayList();
	for (Iterator rtsIter = rts.iterator(); rtsIter.hasNext(); ) {
	    
	    RelationType rtNext = (RelationType) rtsIter.next();
	    if (rtNext.arity() == rt.arity()) {// we can only collapse RelationTypes of same arity
		int j = 0;
		Iterator rtIter = rt.getTypeIter();
		Iterator rtNextIter = rtNext.getTypeIter();
		while (rtIter.hasNext()) {
		    BasicType bt1 = (BasicType) rtIter.next();
		    BasicType bt2 = (BasicType) rtNextIter.next();
		    if (((i == j) && (!_sameSuperType(bt1, bt2))) ||
			((i != j) && (!bt1.equals(bt2))))
			break;
		    j++;
		}

		if (j == rt.arity())
		    ret.add(rtNext);
	    }
	}
	ret.add(rt);
	return ret;
    }
    

    /**
     * @return true if bt1 and bt2 are SigTypes such that bt1.getSuperType() is the
     * same as bt2.getSuperType().  
     **/
    private static boolean _sameSuperType(BasicType bt1, BasicType bt2) {
	if (!((bt1 instanceof SigType) && (bt2 instanceof SigType)))
	    return false;
	else {
	    SigType st1 = (SigType) bt1;
	    SigType st2 = (SigType) bt2;
	    return (st1.getSuperType() == null ? 
		    st2.getSuperType() == null :
		    st1.getSuperType().equals(st2.getSuperType()));
	}
	    
    }
    
    /**
     * @return true if bt is a SigType which is a subtype of an abstract SigType;
     * otherwise returns false.
     **/
    private static boolean _hasAbstractSuperType(BasicType bt) {
	if (bt instanceof SigType) {
	    SigType st  = (SigType) bt;
	    return ((st.getSuperType() != null) && 
		    (st.getSuperType().getSignature().isAbstract()));
	}
	return false;
    }

    /**
     * Returns true if this.size() == 0 or all RelationTypes in this UnionType are empty; 
     * otherwise returns false
     * @return true if this.size() == 0 or for all rt in this, rt.isEmpty(); 
     * otherwise returns false
     **/
    public boolean isEmpty() {
	
	for (Iterator iter = this.getTypeIter(); iter.hasNext(); ) {
	    if (!((RelationType) iter.next()).isEmpty())
		return false;
	}

	return true;

    }

    /**
     * @return true if there exist an r1 in this and r2 in ut such that 
     * r1.arity() == r2.arity() and dom(r1) & dom(r2) is non-empty; 
     * otherwise returns false
     **/
    public boolean canOverride(UnionType ut) {
		
	for (Iterator iter1 = getTypeIter(); iter1.hasNext();) {
	    RelationType r1 = (RelationType) iter1.next();
	    if (ut._arities.contains(new Integer(r1.arity()))) {
		for (Iterator iter2 = ut.getTypeIter(); iter2.hasNext(); ) {
		    RelationType r2 = (RelationType) iter2.next();
		    if ((r1.arity() == r2.arity()) &&
			(!r1.getBasicTypeAt(0).intersect(r2.getBasicTypeAt(0)).isEmpty()))
			return true;
		}
	    }
	}
		
	return false;
    }

    /**
     * @return true if this is a subset of ut:  for all rt in this, there exists
     * a rt' in ut such that rt is a subset of rt';  otherwise returns false.
     **/
    public boolean isSubsetOf(UnionType ut) {

	checkRelationTypesOfThis: for (Iterator iter1 = getTypeIter(); iter1.hasNext(); ) {
	    RelationType rt1 = (RelationType) iter1.next();
	    
	    for (Iterator iter2 = ut.getTypeIter(); iter2.hasNext();) {
		RelationType rt2 = (RelationType) iter2.next();
		if (rt1.isSubsetOf(rt2))
		    continue checkRelationTypesOfThis;
	    }

	    return false;
	}

	return true;
    }

    /**
     * Returns a UnionType u whose RelationTypes are the transpose
     * of the corresponding RelationTypes in this.
     * @return the UnionType, as described above. 
     **/
    public UnionType transpose() {
		
	UnionType ret = new UnionType();
	Iterator iter = this.getTypeIter();
	
	while (iter.hasNext()) {
	    ret.addRelationType(((RelationType) iter.next()).transpose());
	}
	
	return ret;

    }
    /**
     * Computes the union of two UnionTypes. 
     * @return a UnionType u which is the normalized union of this and ut:  
     * u = {rt = rt[0]->rt[1]->...->rt[n-1] | (there exists rt1 in this such that rt == rt1 OR
     * there exists rt2 in ut such that rt == rt2 OR there exist rt1...rtn in this+ut such that
     * the set of tuples described by rt is equivalent to the set of tuples described by
     * rt1+rt2+...+rtn) AND (there is no rt' in u such that rt' & rt is non-empty)}
     **/
    public UnionType union(UnionType ut) {
	       	
	UnionType ret = new UnionType(this);
	for (Iterator iter = ut.getTypeIter(); iter.hasNext(); )
	    ret.addRelationType((RelationType) iter.next());
	return ret;
    }

    /**
     * Computes the intersection of two UnionTypes. 
     * @return a UnionType u whose relation types are the intersection of
     * relation types in this and ut: u = {rt = rt[0]->rt[1]->...->rt[n-1] | there exist rt1
     * in this and rt2 in ut such that rt1.arity() == rt2.arity() == n AND rt == rt1 & rt2}.
     * The result of this operation may be a UnionType of size 0.
     **/
    public UnionType intersect(UnionType ut) {
	       	
	UnionType ret = new UnionType();
		
	for (Iterator thisIter = getTypeIter(); thisIter.hasNext(); ) {
	    RelationType thisRT = (RelationType) thisIter.next();
	    for (Iterator utIter = ut.getTypeIter(); utIter.hasNext(); ) {
		try {
		    ret.addRelationType(thisRT.intersect((RelationType) utIter.next()));
		} catch (InvalidAritiesException iae) {
		    continue; // nothing to do 
		}
	    }
	}

	return ret;
    }

    /**
     * Computes the product of two UnionTypes
     * @param ut UnionType that will be multiplied by this.  
     * @return a UnionType u whose relation types are the product of relation 
     * types in this and ut:  u = {rt = rt[0]->rt[1]->...->rt[n-1] | there exist some rt1 in this
     * and rt2 in ut such that length(rt1) == i AND length(rt2) == j AND n == i + j AND 
     * rt1.isEmpty() == rt2.isEmpty() AND rt[k] = rt1[k] for 0<=k<i AND 
     * rt[k+i] = rt2[k] for 0<=k<j}.  The result of this operation will be a UnionType of 
     * size 0 if this.isEmpty() != ut_.isEmpty().
     **/
    public UnionType product(UnionType ut) {

	UnionType ret = new UnionType();
		
	for (Iterator thisIter = this.getTypeIter(); thisIter.hasNext(); ) {
	    RelationType thisRT = (RelationType) thisIter.next();
	    
	    for (Iterator utIter = ut.getTypeIter(); utIter.hasNext(); ) {
		RelationType utRT = (RelationType) utIter.next();
		if (thisRT.isEmpty() == utRT.isEmpty())
		    ret.addRelationType(thisRT.product(utRT));
	    }
	}

	return ret;
    }
 
    /**
     * Computes the element-wise relational join of this and another UnionType. 
     * @param ut an instance of UnionType
     * @return a UnionType u which is the relational join of this and ut:  
     * u = {rt = rt = rt[0]->rt[1]->...->rt[n-1] | there exist some rt1 in this and rt2 in ut
     * such that length(rt1) == i AND length(rt2) == j AND n == i + j - 1 > 1 AND 
     * rt1[i-1] & rt2[0] is non-empty && rt[k] == rt1[k] for 0<=k<i-1 AND 
     * rt[k+i-1] == rt2[k] for 0<k<j}.  If no RelationType in this is join-compatible with 
     * some RelationType in ut, then a UnionType of size 0 is returned.
     **/
    public UnionType join(UnionType ut) {
		
	UnionType ret = new UnionType();

	for (Iterator thisIter = this.getTypeIter(); thisIter.hasNext(); ) {
	    RelationType rt = (RelationType) thisIter.next();
	    
	    for (Iterator utIter = ut.getTypeIter(); utIter.hasNext(); ) {
		try {
		    ret.addRelationType(rt.join((RelationType) utIter.next()));
		} catch (InvalidJoinException ije) {
		    continue; // nothing to do
		} catch (InvalidAritiesException iae) {
		    continue; // nothing to do
		}
	    }
	}
	
	return ret;
	    
    }


    /**
     * Computes the domain restriction on the RelationTypes of this based
     * on the RelationTypes of ut_ which have arity 1.
     * @param ut_ an instance of UnionType
     * @return a new UnionType u = {rt = rt[0]->rt[1]->...->rt[n-1] | there exist some rt1 in 
     * this and some rt2 in ut such that length(rt1) == n && length(rt2) == 1 && rt1[i] == rt[i] 
     * for 0<i<n && rt[0] == rt1[0] & rt2[0] }.  The result of this computation may be an empty 
     * UnionType or a zero-sized UnionType
     **/
    public UnionType domainRestrict(UnionType ut) {
			
	UnionType ret = new UnionType();

	if ((this.size() > 0) && ut._arities.contains(new Integer(1))) {
	    for (Iterator utIter = ut.getTypeIter(); utIter.hasNext(); ) {
		
		RelationType restrictor = (RelationType) utIter.next();
		if (restrictor.arity() == 1) {
		    for (Iterator thisIter = this.getTypeIter(); thisIter.hasNext();) {
			RelationType rt = (RelationType) thisIter.next();
			ret.addRelationType(rt.columnRestrict(restrictor.getBasicTypeAt(0), 0));
		    }
		}
	    }
	}
							     
	return ret;
    }

    /**
     * Computes the range restriction on the RelationTypes of this based
     * on the RelationTypes of ut_ which have arity 1.
     * @param ut_ an instance of UnionType
     * @return a new UnionType u = {rt = rt[0]->rt[1]->...->rt[n-1] | there exist some rt1 in 
     * this and some rt2 in ut such that length(rt1) == n && length(rt2) == 1 && rt1[i] == rt[i] 
     * for 0<=i<n-1 && rt[n-1] == rt1[n-1] & rt2[0] }.  The result of this computation may be an 
     * empty UnionType or a zero-sized UnionType
     **/
    public UnionType rangeRestrict(UnionType ut) {
			
	UnionType ret = new UnionType();
	
	if ((this.size() > 0) && (ut._arities.contains(new Integer(1)))) {
	    for (Iterator utIter = ut.getTypeIter(); utIter.hasNext(); ) {
		
		RelationType restrictor = (RelationType) utIter.next();
		
		if (restrictor.arity() == 1) {
		    for (Iterator thisIter = this.getTypeIter(); thisIter.hasNext(); ) {
			RelationType rt = (RelationType) thisIter.next();
			ret.addRelationType(rt.columnRestrict(restrictor.getBasicTypeAt(0),
							   rt.arity() - 1));
		    }
		}
	    }
	}
								     
	return ret;

    }
    
    /** 
     * @return a new UnionType u which consists of RelationTypes in this that have
     * the given arity
     **/
    private UnionType extract(int arity) {
	UnionType ret = new UnionType();
	if (_arities.contains(new Integer(arity))) {
	    ret._arities.add(new Integer(arity));
	    for (Iterator iter = getTypeIter(); iter.hasNext() ; ) {
		RelationType rt = (RelationType) iter.next();
		if (rt.arity() == arity)
		    ret._relationTypes.add(rt);
	    }
	}
	return ret;
    }

    /**
     * Returns a UnionType that is transitive closure of arity-2 RelationTypes in this
     * @return a UnionType u such that u = u' + u'.u' + u'.u'.u' + . . . . AND
     * u' = {rt | rt in this AND length(rt) == 2}.  The result of this operation
     * may be a UnionType of size 0 if this contains no RelationTypes of arity 2.
     **/
    public UnionType closure() {
       
	UnionType restrictedType = extract(2);
	UnionType closureType = restrictedType;
	UnionType curType = restrictedType.join(restrictedType);
		
	for (int i = 0; (i<restrictedType.size()) && (!curType.isEmpty()); i++) {
	    closureType = closureType.union(curType);
	    curType = curType.join(restrictedType);
	}
	
	return closureType;
	
    }


    /**
     * @return a new Expr with this as its type, or null if this has size 0.
     **/
    public Expr toExpr() {
	Expr retExpr = null; 
	Iterator iter = this.getTypeIter();
	while (iter.hasNext()) {
	    Expr curExpr = ((RelationType) iter.next()).toExpr();
	    retExpr = (retExpr == null ? 
		       curExpr : 
		       retExpr.union(curExpr));
	}
	
	return retExpr;

    }


    /**
     * If all RelationType in this have the same arity, that arity is returned.
     * If this contains no RelationTypes, the arity is considered to be 0.  
     * Otherwise, a negative integer is returned.
     * @return a non-negative integer x if all RelationType in this have arity x; 0 if
     * this contains no RelationTypes; otherwise returns a negative integer **/

    public int arity() {
	if (_arities.isEmpty())
	    return 0;
	else if (_arities.size() == 1)
	    return ((Integer) _arities.iterator().next()).intValue();
	else
	    return -1;
    }

    /**
     * Returns an unmodifiable set view of Integers that represent the 
     * arities of RelationTypes contained in this
     * @return an unmodifiable set view of Integers that represent the arities 
     * of RelationTypes contained in this
     **/
    public Set arities() {
	return Collections.unmodifiableSet(_arities);
    }

    /**
     * @return true if this contains a RelationType of given arity; otherwise returns false
     **/
    public boolean hasArity(int arity) {
	return _arities.contains(new Integer(arity));
    }

    /**
     * get the number of relation types in this
     * @return the number of basic types
     */
    public int size() {
        return _relationTypes.size();
    }

    /**
     * get an Iterator of the RelationTypes of this
     * @return the Iterator
     */
    public Iterator getTypeIter() {
        return _relationTypes.iterator();
    }

    /**
    public int compareTo(Object obj_) {
	if (equals(obj_)) return 0;     
	return this.toString().compareTo(((UnionType) obj_).toString());
	
    }
    8??

    /**
     * @return if this.size() == 1, the RelationType contained in this 
     * is returned; otherwise, null is returned.
     **/
    public RelationType toRelationType() {
	if (size() == 1)
	    return ((RelationType) getTypeIter().next());
	else
	    return null;
		
    }

    /**
     * Returns an empty UnionType of specified arity.  The returned UnionType will
     * have a single product type of the form EmptyType.EMPTY_TYPE->...->EmptyType.EMPTY_TYPE of 
     * the specified arity.      
     * @param arity the arity of the empty UnionType
     * @return an empty UnionType of specified arity.  The returned UnionType will
     * have a single product type of the form EmptyType.EMPTY_TYPE->...->EmptyType.EMPTY_TYPE of 
     * the specified arity.
     **/
    public static UnionType empty(int arity) {
	Dbg.check(arity > 0);
	return new UnionType(new RelationType(Collections.nCopies(arity, EmptyType.EMPTY_TYPE)));
    }


    /**
     * Check if another object is equal to this.  The object is
     * equal if it is a UnionType with the same relation types as
     * this.
     * @param obj the Object to compare
     * @return <code>true</code> if <code>obj</code> is equal to this; 
     * <code>false</code> otherwise
     */
    public boolean equals(Object obj) {
        if (obj instanceof UnionType) {
            UnionType otherType = (UnionType)obj;
            // must have the same number of basic types
            if ((otherType.size() == this.size()) &&
		(otherType._arities.equals(this._arities))) {
		for (Iterator iter = this.getTypeIter(); iter.hasNext(); ) {
		    if (!otherType._relationTypes.contains(iter.next())) return false;
		}
                return true;
            }
        }

        return false;
    }


    public String toString() {
	
	StringBuffer sb = new StringBuffer("{");
	for (Iterator iter = this.getTypeIter(); iter.hasNext(); ) {
	    sb.append(iter.next());
	    sb.append(iter.hasNext() ? " + " : "");
	}
	sb.append("}");
	return sb.toString();
    }

    public int hashCode() {
	int ret = 0;
	for (Iterator iter = this.getTypeIter(); iter.hasNext(); ) 
	       ret += iter.next().hashCode();
	return ret;
    }
}
